Nuprl Lemma : set_leq_weakening_lt 13,42

s:QOSet, ab:|s|. (a <s b (a  b
latex


Upsets 1
Definitions of StatementDSet, QOSet
Definitionst  T, P  Q, x:AB(x), DSet, QOSet, P & Q, strict_part(x,y.R(x;y);a;b), P  Q,
Lemmasqoset wf, set car wf, set lt wf, set lt is sp of leq

origin